COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	connect to lispax
C00003 00003	useful set theory
C00005 00004	(proof setfacts)
C00011 ENDMK
C⊗;
;connect to lispax
(wipe-out)
(get-proofs lispax)

;we will consider only sets of S-expressions
;XV and YV will have the same declaration as X and Y
;useful set theory
(proof sets)

(decl (av bv) (type: |ground→truthval|))
(decl epsilon (type: |ground⊗@av→truthval|) (infixname: ε) (bindingpower: 925))
(define epsilon |∀av xv.xvεav≡av(xv)|)
(label epsilondef)

(axiom |∀av bv.(∀xv.xvεav≡xvεbv)⊃av=bv|)
(label set_extensionality)

(decl intersection (type: |@av⊗@av→@av|)
      (infixname: ∩) (bindingpower: 950) (prefixname: intersection))
(define intersection |∀av bv.av∩bv=λxv.(av(xv)∧bv(xv))|)
(label interdef)

(decl union (type: |@av⊗@av→@av|)
      (infixname: ∪) (bindingpower: 950) (prefixname: union))
(define union |∀av bv.av∪bv=λxv.(av(xv)∨bv(xv))|)
(label uniondef)

(decl inclusion (type: |@av⊗@av→truthval|)
      (infixname: ⊂) (bindingpower: 920) (prefixname: inclusion))
(define inclusion |∀av bv.av⊂bv≡∀xv.av(xv)⊃bv(xv)|)
(label inclusiondef)

(defax emptyset |emptyset=λxv.false|)
(defax emptyp |∀av.emptyp(av)=∀xv.¬av(xv)|)

;the set of occurrences of an S-exp

(decl mkset (type: |ground→@av|))
(define mkset |∀xv.mkset(xv)=(λyv.yv=xv)|)
(label mkset_def)
(save-proofs set)
(proof setfacts)

;properties of emptyset
(trw |emptyp(emptyset)| (open emptyp emptyset))
;EMPTYP(EMPTYSET)

(trw |∀xv.¬emptyset(xv)| (open emptyset))
;∀XV.¬EMPTYSET(XV)